T, A:Type, f, g:(TAT), L:A List, y, z:T.
(L':A List, a:A.
(L' @ [a]  L  f(list_accum(x,a.f(x,a);y;L'),a) = g(list_accum(x,a.f(x,a);y;L'),a))
 y = z
 list_accum(x,a.f(x,a);y;L) = list_accum(x,a.g(x,a);z;L)  T 

latex

Definitions	t  T, x(s1,s2), x,y. t(x;y), x:A. B(x), list_accum(x,a.f(x;a);y;l), Prop, P  Q, as @ bs, l1  l2, {T}, x. t(x), Top, S  T
Lemmas	iseg weakening, iseg append, list accum append, top wf, last induction, iseg wf, append wf, list accum wf